Improvements to show, and new show from disc#4911
Open
Conversation
ehildenb
reviewed
Apr 22, 2026
Comment on lines
+44
to
+47
| def evict(self) -> None: | ||
| """Release the loaded CTerm from memory.""" | ||
| self._cterm = None | ||
|
|
Member
There was a problem hiding this comment.
I don't actually see where this is used, how does this work? I assume somehow this gets called whenever we're done printing a given node?
ehildenb
reviewed
Apr 22, 2026
Comment on lines
+48
to
+52
| def __eq__(self, other: object) -> bool: | ||
| if isinstance(other, LazyNode): | ||
| return self.id == other.id | ||
| # Also compare with real KCFG.Node | ||
| return hasattr(other, 'id') and self.id == other.id |
Member
There was a problem hiding this comment.
Would this be equivalent anyway?
Suggested change
| def __eq__(self, other: object) -> bool: | |
| if isinstance(other, LazyNode): | |
| return self.id == other.id | |
| # Also compare with real KCFG.Node | |
| return hasattr(other, 'id') and self.id == other.id | |
| def __eq__(self, other: object) -> bool: | |
| return hasattr(other, 'id') and self.id == other.id |
Or perhaps the tighter:
Suggested change
| def __eq__(self, other: object) -> bool: | |
| if isinstance(other, LazyNode): | |
| return self.id == other.id | |
| # Also compare with real KCFG.Node | |
| return hasattr(other, 'id') and self.id == other.id | |
| def __eq__(self, other: object) -> bool: | |
| if isinstance(other, LazyNode): | |
| return self.id == other.id | |
| # Also compare with real KCFG.Node | |
| return isinstance(other, KCFG.Node) and self.id == other.id |
Member
|
Does it make sense to just have lazy-loading be the default anyway, and build it into the main KCFG class? |
Member
|
@claude can you review this PR? And check if |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Memory-efficient proof display: streaming show and lazy loading
Motivation
Displaying large proofs with
kmir showcaused out-of-memory failures. A completed 1411-node proof required 23.8 GB of memory just to print its output, after the proof itself had already finished successfully.Investigation
The initial hypothesis was that the memory cost came from joining the entire output into a single string before printing (
'\n'.join(lines)). Streaming the output line-by-line (via a generator) eliminated this duplication, but peak memory remained at 23.8 GB. The real cost was loading the entire proof into memory, parsing all node CTerms and constraint data from JSON into Python K-term objects, with ~6× memory overhead from Python object representation.Changes
This PR introduces two improvements:
1. Generator-based
show_iterKCFGShow.show_iterandAPRProofShow.show_iteryield lines one at a time instead of collecting them into a list. The existingshowmethods are reimplemented aslist(self.show_iter(...))to avoid code duplication. Tests confirm same output.2. Lazy-loading
show_iter_from_diskAPRProofShow.show_iter_from_diskdisplays a proof without loading the full proof into memory:LazyNode— duck-typesKCFG.Node. Stores node ID, attrs, and a file path. Loads the CTerm fromnodes/{id}.jsononly when.ctermis accessed for printing.LazyCSubst— duck-typesCSubst. Holds the raw JSON dict and defers parsing into K-term objects until.constraintsor.substis accessed.APRProofStub— duck-typesAPRProof. Holds proof metadata (init, target, terminal, bounded, refutations) fromproof.jsonand answers proof-level queries (is_init,is_target,is_terminal, etc.) without loading the KCFG.These stubs are passed into the real
KCFGdata structures (edges, splits, covers, ndbranches accept them via duck typing) and the existingpretty_segmentstraversal works unchanged, with no reimplementation or duplication of the tree-drawing logic.Loading is integrated into the existing code path:
KCFG.from_dictaccepts alazyparameter that controls whether nodes are created asLazyNodestubs and covers useLazyCSubstwrappers.KCFGStore.read_cfg_data_lazyreadskcfg.jsonwithout loading node JSON files.KCFG.read_cfg_data_lazyprovides the entry point, combining the two.Results
Tested on a 1411-node p-token proof (
burn_multisig_n1):show_iter(full load)show_iter_from_disk(lazy)74% memory reduction, 13.5× faster, identical output.
Testing
show_iter_from_diskoutput is compared againstshowoutput in three existingtest_imp.pytest functions (all tests that write proofs to disk). Both default and full-printer modes are exercised.APRProofNodePrinter(proof-level attrs: init, target, terminal).